#include "common.h"
bool bothTrue(bool user1HasActivityFirst,bool user1HasActivitySecond){
    if(user1HasActivityFirst==true){
        if(user1HasActivitySecond==true){
            return true;
        } 
    }else {
        return false;
    }        
}
bool oneTrue(bool user1HasActivityFirst,bool user1HasActivitySecond){
    if(user1HasActivityFirst==true){
        return true;
    }else
    if(user1HasActivitySecond==true){
        return true;
    }
    else {
        return false;
    }        
}
int main() {
	bool saveActivity1Result = false;
	bool saveActivity2Result = false;
	bool user1HasActivityFirst = false;
	bool user1HasActivitySecond = false;
	int user1ScoreFirst = ScoreNotValidated1;
	int user1ScoreSecond = ScoreNotValidated2;//make sure user1ScoreFirst!=user1ScoreSecond
	Activity* pActivityUser1First=NULL;
	Activity* pActivityUser1Second=NULL;

	Activity activity1;

	Activity activity2;

	User user1;


	// printRow_activity(&activity1,"init_1");
	klee_make_symbolic(&activity1, sizeof(activity1), "activity1");
	// printRow_activity(&activity1,"init_2");
	klee_assume(assume_fieldInList_activity_name(&activity1));
	klee_assume(assume_fieldInList_activity_shopId(&activity1));
	klee_assume(assume_fieldInList_activity_on(&activity1));
	klee_assume(assume_fieldInList_activity_newUserScore(&activity1));
	klee_assume(assume_fieldInList_activity_oldUserScore(&activity1));
	klee_assume(assume_betweenFields_activity_newOldUserScoreNotEqual(&activity1));
	// klee_assume(assume_fieldsConstraint_activity_beginDt_endDt( &activity1 ));
    
	klee_make_symbolic(&activity2, sizeof(activity2), "activity2");
	klee_assume(assume_fieldInList_activity_name(&activity2));
	klee_assume(assume_fieldInList_activity_shopId(&activity2));
	klee_assume(assume_fieldInList_activity_on(&activity2));
	klee_assume(assume_fieldInList_activity_newUserScore(&activity2));
	klee_assume(assume_fieldInList_activity_oldUserScore(&activity2));
	klee_assume(assume_betweenFields_activity_newOldUserScoreNotEqual(&activity2));
    
	klee_make_symbolic(&user1, sizeof(user1), "user1");
	klee_assume(assume_fieldInList_user_phone(&user1));
	klee_assume(assume_fieldInList_user_shopId(&user1));
    
	// printRow_activity(&activity1,"before_api_save_row_activity");
	saveActivity1Result = api_save_row_activity(&activity1);
	// printRow_activity(&activity1,"after_api_save_row_activity");
	assert(saveActivity1Result == OK);
	
	// printRow_activity(&activity2,"before_api_save_row_activity");
	saveActivity2Result = api_save_row_activity(&activity2);
	// printRow_activity(&activity2,"after_api_save_row_activity");
	assert(saveActivity2Result == OK);


    
    // printRow_user(&user1,"before_api_hasActivity_1");
	user1HasActivityFirst = api_hasActivity(&user1,&pActivityUser1First);
    printf("user1HasActivityFirst:%d\n", user1HasActivityFirst);
    if(pActivityUser1First!=NULL){
        printRow_activity(pActivityUser1First,"pActivityUser1First");
    }
    // printRow_user(&user1,"after_api_hasActivity_1");
	if(user1HasActivityFirst==true){
		user1ScoreFirst=api_joinActivity(&user1);
        sql_selectTable_user_print();
        // printRow_user(&user1,"after_api_joinActivity_1");
	}

    // printRow_user(&user1,"before_api_hasActivity_2");
	user1HasActivitySecond = api_hasActivity(&user1,&pActivityUser1Second);
    printf("user1HasActivitySecond:%d\n", user1HasActivitySecond);
    if(pActivityUser1Second!=NULL){
        printRow_activity(pActivityUser1Second,"pActivityUser1Second");
    }
    // printRow_user(&user1,"after_api_hasActivity_2");
	if(user1HasActivitySecond==true){
		user1ScoreSecond=api_joinActivity(&user1);
        // printRow_user(&user1,"after_api_joinActivity_2");
	}
    
	klee_assume(oneTrue(user1HasActivityFirst,user1HasActivitySecond));
    
    sql_selectTable_activity_print();
    sql_selectTable_user_print();
    
    printf("user1ScoreFirst:%d,user1ScoreSecond:%d\n", user1ScoreFirst, user1ScoreSecond);
    
    if(user1HasActivityFirst==true){
	if(user1HasActivitySecond==true){
        assert(user1ScoreFirst != user1ScoreSecond);
    }
    }
	
	return 0;
}
